\documentclass[a4paper]{scrartcl}
\usepackage{amsmath,amssymb,fvsw}
\newtheorem{ex}{Exercise}
\newenvironment{exercise}[1]%
   {\def\tmp{}%
    \def\points{#1}%
    \ifx\points\tmp
      \begin{ex}
    \else
      \def\tmp{1}%
    \begin{ex}[#1 point\ifx\points\tmp\else s\fi]
    \fi
    \normalfont
   }%
   {\end{ex}%
   }
   
\usepackage{enumerate}
\newenvironment{subexercises}%
   {\begin{enumerate}[(a)]}%
   {\end{enumerate}}

\renewcommand\paragraph[1]{\medskip\par\noindent\textit{#1}}

\setlength{\parindent}{0pt} % deactivates the indent

\begin{document}
\title{Formal Verification of Software~-- Exercises}
\date{May 2012}
\author{
Thomas Prevedel, 0627595\\
Michael Sobotka, 0826407\\
Alexander Tomsu, 0803543}
\maketitle

\begin{exercise}{1}\label{ex:syntax}
  Show that the \TPL\ program given in exercise~\ref{ex:ifabort}
  is syntactically correct.  
  
\end{exercise}

\textbf{Solution}\\
We show that the program P is syntactically correct by constructing it using our TPL-syntax.

\begin{align*}
P & \Rightarrow P;P \\
  & \stackrel{*}{\Rightarrow} \begin{ALG} \ASS V{E}; \IF\ $E$ \THEN\ P \ELSE\ P \FI \end{ALG} \\
  & \stackrel{*}{\Rightarrow} \begin{ALG} \ASS V{(EBE)}; \IF\ $(EBE)$ \THEN\ \ABORT\ \ELSE\ \WHILE\ $E$ \DO\ P \OD\ \FI \end{ALG} \\
  & \stackrel{*}{\Rightarrow} \begin{ALG} \ASS x{(V+V)}; \IF\ $(V<N)$ \THEN\ \ABORT\ \ELSE\ \WHILE\ $(EBE)$ \DO\ P;P \OD\ \FI \end{ALG} \\
  & \stackrel{*}{\Rightarrow} \begin{ALG} \ASS x{(x+y)}; \IF\ $(x<0)$ \THEN\ \ABORT\ \ELSE\ \WHILE\ $(V\neq V)$ \DO\ \ASS V{$E$}; \ASS V{$E$} \OD\ \FI \end{ALG} \\
  & \stackrel{*}{\Rightarrow} \begin{ALG} \ASS x{(x+y)}; \IF\ $(x<0)$ \THEN\ \ABORT\ \ELSE\ \WHILE\ $(x\neq y)$ \DO\ \ASS V{$(EBE)$}; \ASS V{$(EBE)$} \OD\ \FI \end{ALG} \\
  & \stackrel{*}{\Rightarrow} \begin{ALG} \ASS x{(x+y)}; \IF\ $(x<0)$ \THEN\ \ABORT\ \ELSE\ \WHILE\ $(x\neq y)$ \DO\ \ASS x{$(V+N)$}; \ASS y{$(V+N)$} \OD\ \FI \end{ALG} \\
  & \stackrel{*}{\Rightarrow} \begin{ALG} \ASS x{(x+y)}; \IF\ $(x<0)$ \THEN\ \ABORT\ \ELSE\ \WHILE\ $(x\neq y)$ \DO\ \ASS x{$(x+1)$}; \ASS y{$(y+2)$} \OD\ \FI \end{ALG} \\
  & \approx \begin{ALG} \ASS x{x+y}; \IF\ $x<0$ \THEN\ \ABORT\ \ELSE\ \WHILE\ $x\neq y$ \DO\ \ASS x{$x+1$}; \ASS y{$y+2$} \OD\ \FI \end{ALG} \\
\end{align*} 

\textbf{Conclusion:}\\ 
Since the program P can be constructed using the grammar rules of our TPL-syntax, it is syntactically correct.

\newpage

\begin{exercise}{1}
  Let $\sigma$ be a state satisfying $\sigma(x)=\sigma(y)=1$, and let
  $p$ be the program given in exercise~\ref{ex:ifabort}.
  Compute $\M p\sigma$, using
  \begin{subexercises}
    \item the structural operational semantics
    \item the natural semantics
  \end{subexercises}
  of \TPL.
\end{exercise}

\textbf{Solution}

\begin{subexercises}
	\item \textbf{Structural operational semantics:}
	\begin{align*}
		\begin{ALG}$(p, \sigma) =$ \end{ALG} & \begin{ALG} $(\ASS x{x+y}; \IF$ ..., $\sigma)$\end{ALG}\\
		& \quad \begin{ALG}$(\ASS x{x+y}, \sigma) \Rightarrow \sigma \langle x \mapsto [x+y]\sigma \rangle = \sigma_1$\end{ALG}\\
		\begin{ALG}$\Rightarrow$\end{ALG} &  \begin{ALG}$(\IF\ (x<0)$ \THEN\ ... \ELSE\ ... \FI, $\sigma_1$)\end{ALG}\\
		\Rightarrow & \begin{ALG}(\WHILE\ $x\neq y$ \DO\ ... \OD, $\sigma_1$)\end{ALG}\\
		\Rightarrow & \begin{ALG}(\ASS x{x+1}; \ASS y{y+2}; \WHILE\ ..., $\sigma_1$)\end{ALG}\\
		& \quad \begin{ALG}$(\ASS x{x+1}; \ASS y{y+2}, \sigma_1)$\end{ALG}\\
		& \quad\quad \begin{ALG}$(\ASS x{x+1}, \sigma_1) \Rightarrow \sigma_1 \langle x \mapsto [x+1]\sigma_1 \rangle = \sigma_2$\end{ALG}\\
		& \quad \Rightarrow \begin{ALG}(\ASS y{y+2}, $\sigma_2)$\end{ALG}\\
		\Rightarrow & \begin{ALG}(\ASS y{y+2}; \WHILE \ ..., $\sigma_2$)\end{ALG}\\
		& \quad \begin{ALG}$(\ASS y{y+2}, \sigma_2) \Rightarrow \sigma_2 \langle y \mapsto [y+2]\sigma_2 \rangle = \sigma_3$\end{ALG}\\
		\Rightarrow & \begin{ALG}(\WHILE\ $x\neq y$ \DO\ ... \OD, $\sigma_3$)\end{ALG}\\
		\Rightarrow & \sigma_3
	\end{align*}
	\textbf{States and corresponding values:}
	\begin{align*}
		&\begin{ALG}$\sigma: x \mapsto 1, y \mapsto 2$\end{ALG}\\
		&\begin{ALG}$\sigma_1: x \mapsto [x+y]\sigma = 2, y \mapsto 1$\end{ALG}\\
		&\quad\begin{ALG}$[x<0]\sigma_1 = 0$ (false)\end{ALG}\\
		&\quad\begin{ALG}$[x\neq y]\sigma_1 = 1$ (true)\end{ALG}\\
		&\begin{ALG}$\sigma_2: x \mapsto [x+1]\sigma_1 = 3, y \mapsto 1$\end{ALG}\\
		&\begin{ALG}$\sigma_3: x \mapsto 3, y \mapsto [y+2]\sigma_2 = 3$\end{ALG}\\
		&\quad\begin{ALG}$[x\neq y]\sigma_3 = 0$ (false)\end{ALG}
	\end{align*}
	
	\item \textbf{Natural semantics:}
	\begin{align*}
		\begin{ALG}$[p]\sigma =$\end{ALG} & \begin{ALG}[\ASS x{x+y}; \IF\ ...]$\sigma$\end{ALG}\\
		= & \begin{ALG}[\IF\ ...][\ASS x{x+y}]$\sigma$\end{ALG}\\
		= & \begin{ALG}[\IF\ $(x<0)$ \THEN\ ... \ELSE\ ... \FI\ ]$\sigma_1$\end{ALG}\\
		= & \begin{ALG}[\WHILE\ $x\neq y$ \DO\ ... \OD]$\sigma_1$\end{ALG}\\
		= & \begin{ALG}[\WHILE\ ...][\ASS x{x+1}; \ASS y{y+2}]$\sigma_1$\end{ALG}\\
		= & \begin{ALG}[\WHILE\ ...][\ASS y{y+2}][\ASS x{x+1}]$\sigma_1$\end{ALG}\\
		= & \begin{ALG}[\WHILE\ ...][\ASS y{y+2}]$\sigma_2$\end{ALG}\\
		= & \begin{ALG}[\WHILE\ $x\neq y$ \DO\ ... \OD]$\sigma_3$\end{ALG}\\
		= & \sigma_3
	\end{align*}
	\textbf{States and corresponding values:}
	\begin{align*}
		&\begin{ALG}$\sigma: x \mapsto 1, y \mapsto 2$\end{ALG}\\
		&\begin{ALG}$\sigma_1: x \mapsto [x+y]\sigma = 2, y \mapsto 1$\end{ALG}\\
		&\quad\begin{ALG}$[x<0]\sigma_1 = 0$ (false)\end{ALG}\\
		&\quad\begin{ALG}$[x\neq y]\sigma_1 = 1$ (true)\end{ALG}\\
		&\begin{ALG}$\sigma_2: x \mapsto [x+1]\sigma_1 = 3, y \mapsto 1$\end{ALG}\\
		&\begin{ALG}$\sigma_3: x \mapsto 3, y \mapsto [y+2]\sigma_2 = 3$\end{ALG}\\
		&\quad\begin{ALG}$[x\neq y]\sigma_3 = 0$ (false)\end{ALG}
	\end{align*}
\end{subexercises}

\newpage

\begin{exercise}{1}\label{ex:ifabort}
  Let $p$ be the following program:
  \begin{center}
  \begin{ALG}
    \ASS x{x+y};\\
    \IF\ $x<0$ \THEN\\
    \>\ABORT\\
    \ELSE\\
    \>\WHILE\ $x\neq y$ \DO\\
    \>\>\ASS x{x+1};\\
    \>\>\ASS y{y+2}\\
    \>\OD\\
    \FI
  \end{ALG}
  \end{center}
  Show that $\CA{x=2y\land y>2}p{x=y}$ is totally correct by computing the
  weakest precondition of the program.
\end{exercise}

\textbf{Solution}\\
Let $S_{in}=\{x=2y \wedge y>2\}$ and $S_{out}=\{x=y\}$. 

\begin{align*}
wp(p, S_{out}) & = wp (\ASS x{x+y}, wp(\IF\ \ldots \FI, S_{out})) \\
						   & = wp (\ASS x{x+y}, (x<0 \wedge wp(\ABORT, S_{out})) \vee (x\geq0 \wedge wp(\WHILE \ldots \OD, S_{out}))) \\
						   & = wp (\ASS x{x+y}, (x<0 \wedge false) \vee (x\geq0 \wedge wp(\WHILE \ldots \OD, S_{out}))) \\
							 & = wp (\ASS x{x+y}, (x\geq0 \wedge wp(\WHILE \ldots \OD, S_{out}))) \\
\end{align*}

\textbf{Sub-problem:} Compute the weakest precondition of the while-loop.

\begin{align*}
F_0 & = (x = y \wedge x = y) \\
		& = (x = y) \\
F_1 & = (x \neq y \wedge wp(\ASS x{x+1}; \ASS y{y+2}, F_0)) && \text{$x \neq y$ can be omitted (adds no knowledge)} \\
    & = (x+1 = y+2) \\
F_2 & = (x \neq y \wedge wp(\ASS x{x+1}; \ASS y{y+2}, F_1)) \\
		& = (x+2 = y+4) \\
\end{align*}

According to this observation, we make the following guess and prove it by induction.\\
\textbf{Guess:} $F_i = (x+i = y+2i)$\\
\textbf{Base case:} $F_0 = (x+0 = y+2*0) = (x = y)$ which is indeed true.\\
\textbf{Induction step:} We will compute $F_{i+1}$ and compare it to our guess.

\begin{align*}
F_{i+1} & = (x \neq y \wedge wp(\ASS x{x+1}; \ASS y{y+2}, F_i)) \\
				& = (x \neq y \wedge x+1+i = y+2+2i) \\
				& = x+(i+1) = y+2(i+1) && \text{which is the expected result!}
\end{align*}

We therefore proved: $F_i = (x+i = y+2i) \quad \forall i \geq 0$ \\

Using this knowledge, we can compute the weakest precondition of the while-loop as follows:

\begin{align*}
wp(\WHILE \ldots \OD, S_{out}) & = \exists i (i \geq 0 \wedge F_i) \\
															 & = \exists i (i \geq 0 \wedge x+i=y+2i) \\
															 & = \exists i (i \geq 0 \wedge i = x-y) \\
															 & = \{ x-y \geq 0 \} \\
															 & = \{ x \geq y \}
\end{align*}

Now we can continue with the computation of the weakest precondition of $p$.

\begin{align*}
wp(p, S_{out}) & = wp (\ASS x{x+y}, (x\geq0 \wedge \textbf{wp$(\WHILE \ldots \OD, S_{out})$})) \\
							 & = wp (\ASS x{x+y}, (x\geq0 \wedge x \geq y)) \\
							 & = \{ x+y \geq 0 \wedge x+y \geq y \} \\
							 & = \{ x+y \geq 0 \wedge x \geq 0 \}
\end{align*}

\textbf{Total Correctness:}\\
To show that $\CA{x=2y\land y>2}p{x=y}$ is totally correct, we have to prove the following implication:

\begin{align*}
S_{in} 							& \Rightarrow wp(p, S_{out}) \\
\{x=2y \wedge y>2\} & \Rightarrow \{ x+y \geq 0 \wedge x \geq 0 \}
\end{align*}

We can split the implication into the following two implications:

\begin{align*}
x=2y \wedge y>2 & \Rightarrow x \geq 0 \\
x=2y \wedge y>2 & \Rightarrow x+y \geq 0 
\end{align*}

The first implication holds, because on the left side y must be at least 3 and therefore x must be at least 6, which is of course greater than 0. \\
The second implication holds, because both x and y must be positive. Therefore, their sum is also greater than 0. \\

\textbf{Conclusion:}\\
As the implication holds, we proved that $\CA{x=2y\land y>2}p{x=y}$ is indeed totally correct.

\newpage

\begin{exercise}{1}
  Let $p$ be the program given in exercise~\ref{ex:ifabort}.
  Use the Hoare calculus to show that
  \[\CA{x=2y\land y>2}p{x=y}\]
  is totally correct.
\end{exercise}

\newpage

\begin{exercise}{1}
  Extend our toy language by statements of the form ``$\kw{assert}\
  e$''. When the condition~$e$ evaluates to true, the program
  continues, otherwise the program aborts.

  Specify the syntax and semantics of the extended language.
  Determine the weakest precondition, the weakest liberal
  precondition, the strongest postcondition, and Hoare rules
  (partial and total correctness) for \kw{assert}-statements.
  Show that they are correct.

  Treat the \kw{assert}-statement as a first-class citizen, i.e., do
  not refer to other program statements in the final result.  However,
  you may use other statements as intermediate steps when deriving the
  rules.
\end{exercise}

\textbf{Solution}\\
Please note: To show that the following rules are correct, we will provide their full derivations. Therefore, our rules will be correct by construction.\\

\textbf{Syntax}\\
In addition to all the other rules of the toy language, we define the following rule:

\begin{center}
	$P ::= \kw{assert}\ e$ ($e$ is an expression)
\end{center}

\textbf{Semantics}\\
To define the semantics of the assert-statement, we use the semantics of other, already defined, language constructs.

\begin{align*}
	[\kw{assert}\ e] \sigma & = [\IF\ e \ \THEN\ \SKIP\ \ELSE\ \ABORT\ \FI] \sigma \\
													& = \begin{cases} [\SKIP] \sigma & \text{if} [e] \sigma \neq 0 \\ [\ABORT] \sigma & \text{if} [e] \sigma = 0 \end{cases}
													\intertext{According to the non-existing semantical definition of \ABORT , we omit the abort-branch to leave it undefined on purpose.} \\
													& = [\SKIP] \sigma 		&& \text{if} [e] \sigma \neq 0 \\
													& = \sigma 						&& \text{if} [e] \sigma \neq 0 \\
\end{align*}

\textbf{Weakest Precondition}

\begin{align*}
	wp(\kw{assert}\ e, G) & = wp(\IF\ e \ \THEN\ \SKIP\ \ELSE\ \ABORT\ \FI, G) \\
												& = (e \wedge wp(\SKIP, G)) \vee (\neg e \wedge wp(\ABORT, G)) \\
												& = (e \wedge G) \vee (\neg e \wedge false) \\
												& = e \wedge G
\end{align*}

\textbf{Weakest Liberal Precondition}

\begin{align*}
	wlp(\kw{assert}\ e, G) & = wlp(\IF\ e \ \THEN\ \SKIP\ \ELSE\ \ABORT\ \FI, G) \\
												 & = (e \wedge wlp(\SKIP, G)) \vee (\neg e \wedge wlp(\ABORT, G)) \\
												 & = (e \wedge G) \vee (\neg e \wedge true) \\
												 & = (e \wedge G) \vee \neg e
\end{align*}

\textbf{Strongest Postcondition}

\begin{align*}
	sp(F, \kw{assert}\ e) & = sp(F, \IF\ e \ \THEN\ \SKIP\ \ELSE\ \ABORT\ \FI) \\
												& = sp(F \wedge e, \SKIP) \vee sp(F \wedge \neg e, \ABORT) \\
												& = (F \wedge e) \vee false \\
												& = F \wedge e
\end{align*}

\textbf{Hoare rule (total correctness)} \\
The resulting rule (for total correctness) looks as follows: \\

\begin{center}
$
\ASSERTtotal
		{\CA F {\kw{assert}\ e} G}
		{\CUSTOMFRM{ {F \land e} \lfi {G}}}
		{\CUSTOMFRM{ {F \land \neg e} \lfi {false}}}
$
\end{center}

The rule was derived using Hoare rules for already known language constructs.\\

\begin{center}
\small\infertrue
$
\infer
		{\CA F {\kw{assert}\ e} G}
		{\Ia	{\CA F {\IF\ e \ \THEN\ \SKIP\ \ELSE\ \ABORT\ \FI} G}
				{\Lb
						{\CA {F \land e} {\SKIP} G}
						{\SK {\CA {F \land e} {\SKIP} {F \land e}}}
						{\FRM{1}{ {F \land e} \lfi {G}}}
				}
				{\Lb
						{\CA {F \land \neg e} {\ABORT} G}
						{\FRM{2}{ {F \land \neg e} \lfi {false}}}
						{\ABt {\CA {false} {\ABORT} {G}}}
				}
		}
$
\end{center}

\textbf{Hoare rule (partial correctness)} \\
The Hoare rule for partial correctness looks as follows: \\

\begin{center}
$
\ASSERTpartial
		{\CA F {\kw{assert}\ e} G}
		{\CUSTOMFRM{ {F \land e} \lfi {G}}}
$
\end{center}

The rule looks very similar to the previous rule. It just uses the rule for partial correctness for the abort-statement instead of the rule for total correctness.

\begin{center}
\small\infertrue
$
\infer
		{\CA F {\kw{assert}\ e} G}
		{\Ia	{\CA F {\IF\ e \ \THEN\ \SKIP\ \ELSE\ \ABORT\ \FI} G}
				{\Lb
						{\CA {F \land e} {\SKIP} G}
						{\SK {\CA {F \land e} {\SKIP} {F \land e}}}
						{\FRM{1}{ {F \land e} \lfi {G}}}
				}
				{\AB {\CA {F \land \neg e} {\ABORT} G}}
		}
$
\end{center}


\newpage

\begin{exercise}{1}
  Verify that the following program doubles the value of~$x$.
  For which inputs does it terminate? Choose appropriate pre-
  and postconditions and show that the assertion is totally correct.
  Use $y=2x_0+x$ as a starting point for the invariant,
  where $x_0$ denotes the initial value of~$x$.
\begin{center}
  \begin{ALG}
    \ASS y{3x};\\
    \WHILE\ $2x\neq y$\ \DO\\
    \>\ASS x{x+1};\\
    \>\ASS y{y+1};\\
    \OD
  \end{ALG}
\end{center}    
\end{exercise}

\textbf{Solution.}\\

$Precondition:$ $x=x_0$ is needed to remember the original value of $x$ for the postcondition. Regarding termination, we also need $x \ge 0$. Hence, we obtain 
 \begin{align*}
  S_{in}:  x = x_0 \land x \ge 0
 \end{align*}

$Postcondition:$ Since the original value of x is doubled, we obtain
 \begin{align*}
  S_{out}:  x = 2x_0
 \end{align*}

To show that the loop terminates we have to find a bound function $t$ which
\begin{itemize}
\item is an integer
\item is bounded from below: $ \INV \Rightarrow t \ge 0 $
\item decreases in each iteration in discrete steps
\end{itemize}

The loop condition can be rewritten as $y - 2x \ne 0 $. Since $ y \ge 2x $ (which always holds when analyzing the program), we have in fact $ y - 2x \ge 0 $. These observations suggest
 \begin{align*}
  t :=y - 2x
 \end{align*}
as bound function resp. variant. Since $ t \ge 0 $ only holds when $ y \ge 2x $, we add it to our invariant together with the precondition:

 \begin{align*}
\INV: y=2x_0+x \land x \ge 0 \land y \ge 2x
 \end{align*}

We prove total correctness of our assertions by applying Annotation Calculus (implicitly showing partial correctness and termination).\\
We define $e$ as the loop condition: 
 \begin{align*}
  e := 2x \ne y
 \end{align*}

 \begin{figure}[ht]
   \centering
  \begin{ALG}
\ASSERTN1{S_{in}}\\
\ASSERTN9{\INV\sub{y<-3x}}						\quad(as)$\ua$\\
\ASS y{3x};\\
\ASSERTN3{\INV}								\quad(wht'')\\
\WHILE\ $2x\neq y$\ \DO\\
\>\ASSERTN5{\INV \land e \land t = t_0}					\quad(wht'')\\
\>\ASSERTN8{(\INV \land 0 \le t < t_0) \sub{y<-y+1}\sub{x<-x+1}}	\quad(as)$\ua$\\
\>\ASS x{x+1};\\
\>\ASSERTN7{(\INV \land 0 \le t < t_0) \sub{y<-y+1}}			\quad(as)$\ua$\\
\>\ASS y{y+1};\\
\>\ASSERTN6{\INV \land 0 \le t < t_0}					\quad(wht'')\\
\OD\\
\ASSERTN4{\INV \land \lnot e}						\quad(wht'')\\
\ASSERTN2{S_{out}}
  \end{ALG}
   \caption{Annotation Calculus}
   \label{fig:annotationcalc}
 \end{figure}

It remains to prove the validity of the following three implications:

\begin{itemize}

\item \textbf{1 $\Rightarrow$ 9}\\
$x = x_0 \land x \ge 0 \Rightarrow (y=2x_0+x \land x \ge 0 \land y \ge 2x)\sub{y<-3x}$\\
$x = x_0 \land x \ge 0 \Rightarrow 3x=2x_0+x \land x \ge 0 \land 3x \ge 2x$\\
$x = x_0 \land x \ge 0 \Rightarrow 2x=2x_0 \land x \ge 0 \land 3x \ge 2x$\\

This implication is valid since
\begin{itemize}
\item $x = x_0$ implies $2x = 2x_0$
\item$x \ge 0$ occurs in the premise
\item $x \ge 0$ implies $3x \ge 2x$
\end{itemize}

\item \textbf{5 $\Rightarrow$ 8}\\
$y=2x_0+x \land x \ge 0 \land y \ge 2x \land 2x \ne y \land y-2x=t_0 \Rightarrow (y=2x_0+x \land x \ge 0 \land y \ge 2x \land 0 \le y-2x < t_0)\sub{y<-y+1}\sub{x<-x+1}$\\
$[...] \Rightarrow y+1=2x_0+x+1 \land x+1 \ge 0 \land y+1 \ge 2x +2 \land 0 \le y+1-2x-2 < t_0$\\
$[...] \Rightarrow y=2x_0+x \land x \ge -1 \land y \ge 2x + 1 \land 0 \le y-2x-1 < t_0$\\

This implication is valid since
\begin{itemize}
\item $y=2x_0+x$ occurs in the premise
\item $x \ge 0$ implies $x \ge -1$
\item the two clauses $y \ge 2x \land 2x \ne y$ in the premise yield to $y > 2x$ which satisfies $y \ge 2x + 1$ since we are dealing only with integers
\item $0 \le y-2x-1$ can be rewritten as $y \ge 2x + 1$ which already got satisfied from above
\item $t_0 = y-2x$ implies $y-2x-1 < t_0$
\end{itemize}

\item \textbf{4 $\Rightarrow$ 2}\\
$y=2x_0+x \land x \ge 0 \land y \ge 2x \land 2x=y \Rightarrow x=2x_0$\\

This implication is valid since
\begin{itemize}
\item  $x=2x_0$ can be derived from the premise: The two clauses $y=2x_0+x \land 2x=y$ in the premise yield $2x=2x_0+x$ which further yields $x=2x_0$
\end{itemize}

\end{itemize}

Therefore the assertion is totally correct.

\newpage

\begin{exercise}{1}
    Show that the following correctness assertion is totally correct.
    Describe the function computed by the program if we consider $a$
    as its input and $c$ as its output.
\begin{center}
  \begin{ALG}
    \ASSERTN1{a\geq0}\\
    \ASS b1;\\
    \ASS c0;\\
    \ASSERTN\INV{b=(c+1)^3\land 0\leq c^3\leq a}\\
    \WHILE\ $b\leq a$\ \DO\\
    \>\ASS d{3*c+6};\\
    \>\ASS c{c+1};\\
    \>\ASS b{b+c*d+1}\\
    \OD\\
    \ASSERTN2{c^3\leq a<(c+1)^3}
  \end{ALG}
\end{center}    
\end{exercise}

\textbf{Solution.}\\

We prove total correctness by applying annotation calculus which implicitly shows partial correctness and termination. Since the invariant is already given, we continue to add intermediate conditions as seen in figure \ref{fig:annotationcalc2}.\\

To show that the loop terminates we have to find a bound function $t$ which
\begin{itemize}
\item is an integer
\item is bounded from below: $ \INV \Rightarrow t \ge 0 $
\item decreases in each iteration in discrete steps
\end{itemize}

The loop condition can be rewritten as $a - b \ge 0$. This suggests
 \begin{align*}
  t :=a - b
 \end{align*}
as bound function resp. variant.\\

We define $e$ as the loop condition:
 \begin{align*}
  e := b \le a
 \end{align*}

 \begin{figure}[ht]
   \centering
  \begin{ALG}
\ASSERTN1{a\geq0}\\
\ASSERTN{10}{\INV\sub{c<-0}\sub{b<-1}}									\quad(as)$\ua$\\
\ASS b1;\\
\ASSERTN9{\INV\sub{c<-0}}											\quad(as)$\ua$\\
\ASS c0;\\
\ASSERTN\INV{b=(c+1)^3\land 0\leq c^3\leq a}\\
\WHILE\ $b\leq a$\ \DO\\
\>\ASSERTN4{\INV \land e \land t=t_0}									\quad(wht''')\\
\>\ASSERTN8{(\INV \land (e \Rightarrow 0 \le t < t_0))\sub{b<-b+cd+1}\sub{c<-c+1}\sub{d<-3c+6}}	\quad(as)$\ua$\\
\>\ASS d{3*c+6};\\
\>\ASSERTN7{(\INV \land (e \Rightarrow 0 \le t < t_0))\sub{b<-b+cd+1}\sub{c<-c+1}}			\quad(as)$\ua$\\
\>\ASS c{c+1};\\
\>\ASSERTN6{(\INV \land (e \Rightarrow 0 \le t < t_0))\sub{b<-b+cd+1}}					\quad(as)$\ua$\\
\>\ASS b{b+c*d+1}\\
\>\ASSERTN5{\INV \land (e \Rightarrow 0 \le t < t_0)}							\quad(wht''')\\
\OD\\
\ASSERTN3{\INV \land \lnot e}										\quad(wht''')\\
\ASSERTN2{c^3\leq a<(c+1)^3}
  \end{ALG}
   \caption{Annotation calculus for exercise 7}
   \label{fig:annotationcalc2}
 \end{figure}

\newpage
It remains to prove the validity of the following three implications:

\begin{itemize}

\item \textbf{1 $\Rightarrow$ 10}\\
$a \ge 0 \Rightarrow (b=(c+1)^3\land 0\leq c^3\leq a)\sub{c<-0}\sub{b<-1}$\\
$a \ge 0 \Rightarrow 1=1 \land 0\leq 0 \leq a$\\

This implication is valid since
\begin{itemize}
\item $1=1$ is true
\item $0 \le 0$ is true
\item $0 \leq a$ occurs in the premise
\end{itemize}

\newpage

\item \textbf{4 $\Rightarrow$ 8}\\
$b=(c+1)^3 \land 0\leq c^3\leq a \land b \le a \land a-b=t_0 \Rightarrow (b=(c+1)^3 \land 0 \leq c^3\leq a \land ((b \le a) \Rightarrow (0 \le a-b < t_0)))\sub{b<-b+cd+1}\sub{c<-c+1}\sub{d<-3c+6}$\\

To shorten our proof we denote the the premise of this formula with $Prem$.

$Prem \Rightarrow (b+cd+1=(c+1)^3 \land 0 \leq c^3\leq a \land ((b+cd+1 \le a) \Rightarrow (0 \le a-b-cd-1 < t_0)))\sub{c<-c+1}\sub{d<-3c+6}$\\
$Prem \Rightarrow (b+cd+d+1=(c+2)^3 \land 0 \leq (c+1)^3\leq a \land ((b+cd+d+1 \le a) \Rightarrow (0 \le a-b-cd-d-1 < t_0)))\sub{d<-3c+6}$\\
$Prem \Rightarrow b+3c^2+6c+3c+6+1=(c+2)^3 \land 0 \leq (c+1)^3\leq a \land ((b+3c^2+6c+3c+6+1 \le a) \Rightarrow (0 \le a-b-3c^2-6c-3c-6-1 < t_0))$\\
$Prem \Rightarrow b+3c^2+9c+7=(c+2)^3 \land 0 \leq (c+1)^3\leq a \land ((b+3c^2+9c+7 \le a) \Rightarrow (0 \le a-b-3c^2-9c-7 < t_0))$\\

We notice that $0 \leq c^3$ in the premise implies $c \ge 0$ which we will use in the following.\\
\textit{Note: In each following subpoint we will derive a clause in the conclusion (from left to right).}\\

This implication is valid (for the first 3 clauses in the conclusion) since
\begin{itemize}
\item the following holds: We substitute $b=(c+1)^3$ from the premise into the clause $b+3c^2+9c+7=(c+2)^3$ from the conclusion. This yields\\ $(c+1)^3+3c^2+9c+7=(c+2)^3$ which can be rewritten as\\ $c^3+3c^2+3c+1+3c^2+9c+7=c^3+6c^2+12c+8$ which again is\\ $c^3+6c^2+12c+8=c^3+6c^2+12c+8$ which is true.
\item $0 \leq (c+1)^3$ in the premise can be rewritten as $c \ge -1$ which can be derived from the clause $c \ge 0$ in the premise
\item  $(c+1)^3\leq a$ can be derived from the two clauses $b=(c+1)^3 \land b \le a$ in the premise
\end{itemize}

We have derived the first 3 clauses in the conclusion, it remains to prove the following:

$Prem \Rightarrow (b+3c^2+9c+7 \le a) \Rightarrow (0 \le a-b-3c^2-9c-7 < t_0)$\\

By applying deduction theorem we get

$Prem \land (b+3c^2+9c+7 \le a) \Rightarrow (0 \le a-b-3c^2-9c-7 < t_0)$\\

\textit{Note: In each following subpoint we will derive a clause in the conclusion (from left to right).}\\

This implication is valid since
\begin{itemize}
\item the following holds: We substitute $b=(c+1)^3$ from $Prem$ into the clause $b+3c^2+9c+7 \le a$ from the premise and into the clause $0 \le a-b-3c^2-9c-7$ from the conclusion.\\In the premise this yields $(c+1)^3 +3c^2+9c+7 \le a$.
In the conclusion this yields $0 \le a-(c+1)^3-3c^2-9c-7$ which can be rewritten as $(c+1)^3 +3c^2+9c+7 \le a$ which can be derived from the same clause in the premise
\item the following holds: We substitute $t_0=a-b$ from the premise into the clause $a-b-3c^2-9c-7 < t_0$ from the conclusion. This yields $a-b-3c^2-9c-7 < a-b$ which can be rewritten as $0 < 3c^2+9c+7$. This can clearly be derived from the clause $c \ge 0$ in the premise
\end{itemize}

\item \textbf{3 $\Rightarrow$ 2}\\
$b=(c+1)^3\land 0\leq c^3\leq a \land b > a \Rightarrow c^3\leq a<(c+1)^3$\\

This implication is valid since
\begin{itemize}
\item $c^3\leq a$ occurs in the premise
\item $a<(c+1)^3$ can be derived from the two clauses $b=(c+1)^3 \land b > a$ in the premise
\end{itemize}

\end{itemize}

Therefore the assertion is totally correct.\\

\textit{Function computed by the program.} It is sufficient to analyze the postcondition, which expresses exactly those properties of the program we are interested in. Taking the cube root, we obtain $c \le \sqrt[3]{a} < c+1$, which is the same as $c=\lfloor \sqrt[3]{a} \rfloor$. Hence the program computes the cube root rounded down to an integer.

\newpage

\begin{exercise}{1}
  Prove that the rule
\[
\begin{array}{c}
\WH{\CA{\INV}{\WHILE\ e\ \DO\ p\ \OD}{\INV\land\lnot e}}%
   {\CA{\INV\land e}{p}{\INV}}
\end{array}
\]
is correct regarding partial correctness, i.e., show that
$\CA{\INV}{\WHILE\ e\ \DO\ p\ \OD}{\INV\land\lnot e}$ is partially correct
whenever $\CA{\INV\land e}{p}{\INV}$ is partially correct.
\end{exercise}
\newpage

\begin{exercise}{2}
  Determine the weakest liberal precondition of \WHILE-loops, i.e.,
  find a formula equivalent to $\WLP(\WHILE\ e\ \DO\ p\ \OD, G)$
  similar to the weakest precondition in the course.

  Use your formula to compute the weakest liberal precondition of
  the program 
  \begin{center}
     \ASS z0;
     \WHILE\ $y\neq0$ \DO
       \ASS z{z+x};
       \ASS y{y-1}
     \OD
  \end{center}
  with respect to the postcondition $z=x*y_0$. Compare the result
  to the weakest precondition computed in the course and explain
  the differences.
\end{exercise}

\textbf{Solution}\\

\textbf{Weakest liberal precondition} wlp($p$, $G$)\textbf{:} Given a propram $p$ and a postcondition $G$,
characterize all input states such that either $p$ does not terminate or $G$ holds afterwards.\\
$\Rightarrow$ \textbf{wlp($p$, $G$)} = $\{\sigma\in G | [p]\sigma$ undefined or $[p]\sigma\in G \}$\\

$\Rightarrow$ \textbf{wlp(\WHILE\ $e$ \DO\ $p$ \OD, $G$)}: All states such that loop does not terminate
or all states such that loop terminates after a finite number of iterations in a $G$-state.\\

$\{F_i\}$ ... set of states such that $p$ executes $i$ times and leads to $G$-state\\
\begin{align*}
	\textbf{0 iterations:} & & \begin{ALG}$F_0 = \neg e \wedge G$\end{ALG}\\
	\textbf{1 iteration:} & & \begin{ALG}$F_1 = e$ $\wedge$ wlp($p$, $F_0$)\end{ALG}\\
	\textbf{2 iterations:} & & \begin{ALG}$F_2 = e$ $\wedge$ wlp($p$, $F_1$)\end{ALG}\\
	...&&...\\
	...&&...\\
	...&&...\\
	\textbf{i iterations:} & & \begin{ALG}$F_i = e$ $\wedge$ wlp($p$, $F_{i-1}$)\end{ALG}\\ 
\end{align*}
$\{F_i\} = \{e$ $\wedge$ wlp$(p, F_{i-1})\}$ ... set of states such that
\begin{itemize}
	\item $p$ is executed once (because $e$ is true), resulting in a state where
	\item $i - 1$ further iterations will lead to a G-state.
\end{itemize}

$\Rightarrow$ \textbf{wlp(\WHILE\ $e$ \DO\ $p$ \OD, $G$)} $=  (F_0 \vee F_1 \vee F_2 \vee$ ...) $\vee$ $\neg(F_0 \vee F_1 \vee F_2 \vee$ ...)   $= \exists i (i \ge 0$ $\wedge$ $F_i)$ $\vee$ $\neg\exists i (i \ge 0$ $\wedge$ $F_i)$

\end{document}

